$\forall$${\it da}$:$k$:Knd fp$\rightarrow$ Type, $k$:Knd. Normal(${\it da}$) $\Rightarrow$ $k$ $\in$ dom(${\it da}$) $\Rightarrow$ Normal(${\it da}$($k$)?Void)